Nuprl Lemma : one_ideal_wf
13,42
postcript
pdf
r
:CRng{i}. (1
r
)
Ideal(
r
){1}
latex
Up
rings
1
Definitions of Statement
(1
r
)
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Ideal(
r
){i}
,
(1
r
)
,
S
Ideal of
R
,
True
,
P
&
Q
,
P
Q
,
s
SubGrp of
g
,
r
+gp
,
|
g
|
,
t
.1
,
,
S
T
,
suptype(
S
;
T
)
,
CRng
,
Rng
Lemmas
crng
wf
,
true
wf
,
rng
car
wf
,
ideal
p
wf
origin
r:CRng{i}. (1r) 
Ideal(r){1} r:CRng{i}. (1r) Ideal(r){1} x:A. B(x) T
Q
+gp
T